w:World, e, e':E. FairFifo  e < e'  time(e)<time(e') 

latex

Definitions	x f y, i=j, t  T, {T}, P  Q, x:A. B(x), SQType(T), , s = t, Prop, s ~ t, #$n, left+right, P  Q, Dec(P), a<b, E, w-pred(w;e), x.A(x), w-info(w;e), Id, pred!(e;e'), AB, Void, x:AB(x), False, A, {x:A| B(x) }, , rel_exp(T;R;n), f(a), time(e), , x:AB(x), x:A. B(x), R^+, e < e', World, FairFifo, P & Q, n-m, b, b, , P  Q, Unit, -n, n+m
Lemmas	eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, w-pred!-decreases, cless wf, fair-fifo wf, world wf, nat plus properties, w-time wf, nat wf, rel exp wf, le wf, pred! wf, Id wf, w-info wf, w-pred wf, w-E wf, decidable int equal